feat: Voronovskaja-type formula for the Bézier variant of the Bernstein operators #1444

shamEiNew · 2026-01-02T11:14:38Z

This PR attempts to add the problem of Bézier-Bernstein operators from this source

Open problem:
For $\alpha \neq 1$, prove the existence of a Voronovskaja-type asymptotic formula and determine the limit
$\lim_{n \to \infty } \sqrt{n} \, \big (B_{ n,\alpha} f(x)-f(x) \big)$
for suitable smooth functions $f$. Where

$$(B_{n,\alpha}f)(x) = \sum_{k=0}^{n} f\!\left(\frac{k}{n}\right) \left(J_{n,k}^\alpha(x)-J_{n,k+1}^\alpha(x)\right),$$

where
$J_{n,k}(x)=\sum_{j=k}^{n} \binom{n}{j}x^j(1-x)^{n-j}.$

Questions: Do I need to add the proof of classical case when $\alpha = 1$.

YaelDillies · 2026-01-03T10:53:51Z

FormalConjectures/Paper/VoronovskajaTypeFormula.lean

+and $J_{n,n+1}(x) = 0$.
+
+In the classical case $\alpha = 1$, these operators reduce to the usual Bernstein operators.
+For sufficiently smooth $f$ one  has the classical Voronovskaja asymptotic formula


Suggested change

For sufficiently smooth $f$ one has the classical Voronovskaja asymptotic formula

For sufficiently smooth $f$, one has the classical Voronovskaja asymptotic formula

YaelDillies · 2026-01-03T10:54:49Z

FormalConjectures/Paper/VoronovskajaTypeFormula.lean

+    If the limit exists, determine an explicit expression for it in terms of $f$, $x$, and $\alpha$.
+-/
+
+/-!


This is the syntax for a module doc. For a docstring, you instead need to do

Suggested change

/-!

/--

YaelDillies · 2026-01-03T10:54:56Z

FormalConjectures/Paper/VoronovskajaTypeFormula.lean

+/-!
+Cumulative sum `J_{n,k}(x) = ∑_{j=k}^n p_{n,j}(x)`
+-/
+noncomputable def J (n k : ℕ) (x : ℝ ) : ℝ  :=


Suggested change

noncomputable def J (n k : ℕ) (x : ℝ ) : ℝ :=

noncomputable def J (n k : ℕ) (x : ℝ) : ℝ :=

YaelDillies · 2026-01-03T10:55:59Z

FormalConjectures/Paper/VoronovskajaTypeFormula.lean

+noncomputable def J (n k : ℕ) (x : ℝ ) : ℝ  :=
+∑ j ∈ Finset.Icc k n, Polynomial.eval x (bernsteinPolynomial ℝ n j)


Does this polynomial have a name in the literature? Do you think you should define it as a polynomial?

I guess it may be called Bernstein tail polynomial would be suitable. I think it can be defined as a polynomial, should I do it?

Yes please!

Changed it to Polynomial in the latest commit

YaelDillies · 2026-01-03T10:56:16Z

FormalConjectures/Paper/VoronovskajaTypeFormula.lean

+@[category research solved, AMS 26 40 47]
+theorem voronovskaja_theorem.bernstein_operators
+    (f : ℝ → ℝ) (x : ℝ) (hx : x ∈ I)
+    (f'' : ℝ := iteratedDerivWithin 2 f I x):


Suggested change

(f'' : ℝ := iteratedDerivWithin 2 f I x):

(f'' : ℝ := iteratedDerivWithin 2 f I x) :

YaelDillies · 2026-01-03T10:56:27Z

FormalConjectures/Paper/VoronovskajaTypeFormula.lean

+
+/-!
+Conjecture: Voronovskaja-type formula for Bézier-Bernstein operators
+with shape parameter α ≠ 1.  -/


Suggested change

with shape parameter α ≠ 1. -/

with shape parameter α ≠ 1. -/

YaelDillies · 2026-01-09T11:37:54Z

FormalConjectures/Paper/VoronovskajaTypeFormula.lean

+noncomputable def BernsteinTail (n k : ℕ) : Polynomial ℝ :=
+  ∑ j ∈ Finset.Icc k n,
+    bernsteinPolynomial ℝ n j


Suggested change

noncomputable def BernsteinTail (n k : ℕ) : Polynomial ℝ :=

∑ j ∈ Finset.Icc k n,

bernsteinPolynomial ℝ n j

noncomputable def bernsteinTail (n k : ℕ) : ℝ[X] :=

∑ j ∈ .Icc k n, bernsteinPolynomial ℝ n j

YaelDillies · 2026-01-09T11:38:07Z

FormalConjectures/Paper/VoronovskajaTypeFormula.lean

+Bézier–type Bernstein operator:
+`(B_{n,α} f)(x) = ∑_{k=0}^n f(k/n) * (J_{n,k}(x)^α - J_{n,k+1}(x)^α)`
+-/
+noncomputable def BezierBernstein (n : ℕ) (α : ℝ) (f : ℝ  → ℝ) (x : ℝ) : ℝ :=


Suggested change

noncomputable def BezierBernstein (n : ℕ) (α : ℝ) (f : ℝ → ℝ) (x : ℝ) : ℝ :=

noncomputable def bezierBernstein (n : ℕ) (α : ℝ) (f : ℝ → ℝ) (x : ℝ) : ℝ :=

YaelDillies · 2026-01-09T11:39:02Z

FormalConjectures/Paper/VoronovskajaTypeFormula.lean

+∑ k ∈  Finset.range (n+1),
+    f (k/n) * (((BernsteinTail n k).eval x) ^ α - ((BernsteinTail n k + 1).eval x) ^ α)


Suggested change

∑ k ∈ Finset.range (n+1),

f (k/n) * (((BernsteinTail n k).eval x) ^ α - ((BernsteinTail n k + 1).eval x) ^ α)

∑ k ∈ .range (n+1),

f (k/n) * ((bernsteinTail n k).eval x ^ α - (bernsteinTail n k + 1).eval x ^ α)

YaelDillies · 2026-01-09T11:40:48Z

FormalConjectures/Paper/VoronovskajaTypeFormula.lean

+    (f : ℝ → ℝ) (x : ℝ) (hx : x ∈ I)
+    (f'' : ℝ := iteratedDerivWithin 2 f I x) :
+    Tendsto (fun (n : ℕ) => n • (BezierBernstein n 1 f x - f x))


This doesn't do at all what you think. This is the syntax for a default value. You instead want

Suggested change

(f : ℝ → ℝ) (x : ℝ) (hx : x ∈ I)

(f'' : ℝ := iteratedDerivWithin 2 f I x) :

Tendsto (fun (n : ℕ) => n • (BezierBernstein n 1 f x - f x))

(f : ℝ → ℝ) (x : ℝ) (hx : x ∈ I) :

let f'' : ℝ := iteratedDerivWithin 2 f I x

Tendsto (fun (n : ℕ) => n • (BezierBernstein n 1 f x - f x))

YaelDillies · 2026-01-09T11:41:07Z

FormalConjectures/Paper/VoronovskajaTypeFormula.lean

+theorem voronovskaja_theorem.bezier_bernstein_operators
+    (α : ℝ) (hα : α ≠ 1)
+    (f : ℝ → ℝ) (x : ℝ) (hx : x ∈ I)
+    (f'' : ℝ := iteratedDerivWithin 2 f I x)


YaelDillies · 2026-01-10T13:10:20Z

FormalConjectures/Paper/VoronovskajaTypeFormula.lean

+
+This is already in the literature; here we state it.


No need to write this, the tag already contains this info

Suggested change

This is already in the literature; here we state it.

YaelDillies · 2026-01-10T13:11:31Z

FormalConjectures/Paper/VoronovskajaTypeFormula.lean

+Classical Voronovskaja theorem (α = 1)
+
+For smooth `f`, the limit:
+    n * (B_n f x - f x) → (1/2)*x*(1-x)*f''(x)


Can you latex this?

YaelDillies · 2026-01-10T13:11:46Z

FormalConjectures/Paper/VoronovskajaTypeFormula.lean

+
+/--
+Bézier–type Bernstein operator:
+`(B_{n,α} f)(x) = ∑_{k=0}^n f(k/n) * (J_{n,k}(x)^α - J_{n,k+1}(x)^α)`


YaelDillies · 2026-01-10T13:12:51Z

FormalConjectures/Paper/VoronovskajaTypeFormula.lean

+
+*References:*
+
+* [A problem in Constructive theory of functions, Szopol 2010](https://www.math.bas.bg/mathmod/Proceedings_CTF/CTF-2010/files_CTF-2010/Open_problems.pdf?utm_source=perplexity)


Can you put this at the end of the doc?

theorem added

27713e8

YaelDillies changed the title ~~Add Voronovskaja-type Formula for the Bezier Variant of the Bernstein Operators~~ feat: Voronovskaja-type formula for the Bézier variant of the Bernstein operators Jan 3, 2026

YaelDillies reviewed Jan 3, 2026

View reviewed changes

YaelDillies added the awaiting-author The author should answer a question or perform changes. Reply when done. label Jan 3, 2026

shamEiNew added 2 commits January 8, 2026 16:24

fixed typos

f161035

rw J as Polynomial

0d6b8e8

YaelDillies reviewed Jan 9, 2026

View reviewed changes

fixed definition of f''

a685ec6

YaelDillies reviewed Jan 10, 2026

View reviewed changes

	For sufficiently smooth $f$ one has the classical Voronovskaja asymptotic formula
	For sufficiently smooth $f$, one has the classical Voronovskaja asymptotic formula

	noncomputable def J (n k : ℕ) (x : ℝ ) : ℝ :=
	noncomputable def J (n k : ℕ) (x : ℝ) : ℝ :=

		noncomputable def J (n k : ℕ) (x : ℝ ) : ℝ :=
		∑ j ∈ Finset.Icc k n, Polynomial.eval x (bernsteinPolynomial ℝ n j)

	(f'' : ℝ := iteratedDerivWithin 2 f I x):
	(f'' : ℝ := iteratedDerivWithin 2 f I x) :

	with shape parameter α ≠ 1. -/
	with shape parameter α ≠ 1. -/

	noncomputable def BezierBernstein (n : ℕ) (α : ℝ) (f : ℝ → ℝ) (x : ℝ) : ℝ :=
	noncomputable def bezierBernstein (n : ℕ) (α : ℝ) (f : ℝ → ℝ) (x : ℝ) : ℝ :=

		∑ k ∈ Finset.range (n+1),
		f (k/n) * (((BernsteinTail n k).eval x) ^ α - ((BernsteinTail n k + 1).eval x) ^ α)


		References:

		* [A problem in Constructive theory of functions, Szopol 2010](https://www.math.bas.bg/mathmod/Proceedings_CTF/CTF-2010/files_CTF-2010/Open_problems.pdf?utm_source=perplexity)

feat: Voronovskaja-type formula for the Bézier variant of the Bernstein operators #1444

Are you sure you want to change the base?

feat: Voronovskaja-type formula for the Bézier variant of the Bernstein operators #1444

Uh oh!

Conversation

shamEiNew commented Jan 2, 2026 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

shamEiNew commented Jan 2, 2026 •

edited by YaelDillies

Loading